send_onceR{$done:ut2, $tg:ut2, $b:ut2, $done1:ut2}
send_onceR(T; A; f; l)
== ([onceR{$b:ut2, $done1:ut2}
== ([onceR(source(l))
== (; sends locl("$b")(v:Unit) on l:
== (; tagged([<"$tg",s,v. [f(s("$done"))]>],State("$done" : A),v):"$tg" : T]) 

latex

---

clarification:

send_onceR{$done:ut2, $tg:ut2, $b:ut2, $done1:ut2}
send_onceR(T; A; f; l)
== (onceR{$b:ut2, $done1:ut2}
== (onceR(source(l))
== (.sends locl("$b")(v:Unit) on l:
== (.tagged(<"$tg",s,v. (f(s("$done"))).nil>.nil,State("$done" : A),v):"$tg" : T
== (..nil) 

latex

Definitions

(L), onceR{$a:ut2, $done:ut2}(i), source(l), sends knd(v:T) on l:tagged(g,State(ds),v):dt, locl(a), Unit, x : v, <a,b>, x.A(x), car.cdr, f(a), "$x", nil